perm filename EQUAL.LSP[S84,JMC] blob
sn#756743 filedate 1984-06-03 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00005 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 equal.lsp[s84,jmc] Circumscribing equality
C00010 00003 labels: SIMPINFO
C00015 00004 This proof uses circumscription to maximize the uniqueness of names, through
C00025 00005 labels: SIMPINFO
C00033 ENDMK
C⊗;
;equal.lsp[s84,jmc] Circumscribing equality
(proof unique_names)
1. (axiom |index a = 1 ∧ index b = 2 ∧ index c = 3 ∧ index d = 4|)
(label simpinfo)
2. (der |¬(1=2) ∧ ¬(1=3) ∧ ¬(2=3) ∧ ¬(1=4) ∧ ¬(2=4) ∧ ¬(2=4)|)
(label simpinfo)
3. (define equiv |∀e.equiv e ≡ (∀x.e(x,x)) ∧ (∀x y.e(x,y) ⊃ e(y,x))
∧ (∀x y z.e(x,y) ∧ e(y,z) ⊃ e(x,z))|)
;e(x,y) is our imitation equality.
4. (define ax |∀e.ax e ≡ e(a,b) ∧ equiv e|)
5. (define ax1 |∀e.ax1 e ≡ ax e ∧ ∀e1.(ax e1 ∧ (∀x y.e1(x,y) ⊃ e(x,y))
⊃ (∀x y.e(x,y) ≡ e1(x,y)))|)
6. (assume |ax1(e0)|)
7. (define e2 |∀x y.e2(x,y) ≡ x = a ∧ y = b ∨ x=b ∧ y=a ∨ x = y|)
(der-slow)
8. (der |equiv e2| nil (open equiv) (open e2))
9. (der |ax e2| (8) (open ax) (open e2))
10. (rw 6 (open ax1))
11. (der unique_names#10#1 10)
12. (rw 11 (open ax))
13. (rw 12 (open equiv))
;14. (der |∀x y.e2(x,y) ⊃ e0(x,y)| (13) (open e2))
14. (der |∀x y.x=a ∧ y=b ⊃ e0(x,y)| (13))
15. (der |∀x y.x=b ∧ y=a ⊃ e0(x,y)| (13))
16. (der |∀x y.x=y ⊃ e0(x,y)| (13))
17. (assume |(∀x y.q2(x,y) ≡ p1(x,y) ∨ p2(x,y) ∨ p3(x,y))|) (label xx)
18. (der |(∀x y.p1(x,y) ⊃ q0(x,y))∧(∀x y.p2(x,y) ⊃ q0(x,y))
∧(∀x y.p3(x,y) ⊃ q0(x,y))
⊃ (∀x y.q2(x,y) ⊃ q0(x,y))|
()
(use xx mode: always))
19. (ci xx *)
;20. (trw |∀p1 p2 p3 q0 q2.unique_names#19| (19))
;20. (assume |∀p1 p2 p3 q0 q2.unique_names#19| (19))
;(print (proof-freevars 19))
20. (ue ((p1.|λx y.x=a∧y=b|)
(p2.|λx y.x=b∧y=a|)
(p3.|λx y.x=y|)
(q0.|e0|)
(q2.|e2|)))
(der-fast)
21. (der |∀x y.e2(x,y) ⊃ e0(x,y)| (20 14 15 16) (open e2))
22. (der |∀e1.ax e1 ∧ (∀x y.e1(x,y) ⊃ e0(x,y)) ⊃ (∀x y.e0(x,y) ≡ e1(x,y))|
(10))
23. (ue ((e1.|e2|)) 22)
24. (der |∀x y.e0(x,y) ≡ e2(x,y)| (9 21 23))
25. (rw * (open e2))
(der-slow)
26. (der |a ≠ b| (1 2))
;labels: SIMPINFO
1. (AXIOM |INDEX(A)=1∧INDEX(B)=2∧INDEX(C)=3∧INDEX(D)=4|)
;labels: SIMPINFO
2. (DERIVE |¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4| () NIL)
;¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4
3. (DEFINE EQUIV
|∀E.EQUIV(E)≡
(∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))|
NIL)
4. (DEFINE AX |∀E.AX(E)≡E(A,B)∧EQUIV(E)| NIL)
5. (DEFINE AX1
|∀E.AX1(E)≡
AX(E)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))|
NIL)
6. (ASSUME |AX1(E0)|)
;deps: (6)
7. (DEFINE E2 |∀X Y.E2(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y| NIL)
8. (DERIVE |EQUIV(E2)| () ((OPEN EQUIV) (OPEN E2)))
;EQUIV(E2)
9. (DERIVE |AX(E2)| (8) ((OPEN AX) (OPEN E2)))
;AX(E2)
10. (RW 6 (OPEN AX1))
;AX(E0)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
;deps: (6)
11. (DERIVE |AX(E0)| (10) NIL)
;AX(E0)
;deps: (6)
12. (RW 11 (OPEN AX))
;E0(A,B)∧EQUIV(E0)
;deps: (6)
13. (RW 12 (OPEN EQUIV))
;E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
;deps: (6)
14. (DERIVE |∀X Y.X=A∧Y=B⊃E0(X,Y)| (13) NIL)
;∀X Y.X=A∧Y=B⊃E0(X,Y)
;deps: (6)
15. (DERIVE |∀X Y.X=B∧Y=A⊃E0(X,Y)| (13) NIL)
;∀X Y.X=B∧Y=A⊃E0(X,Y)
;deps: (6)
16. (DERIVE |∀X Y.X=Y⊃E0(X,Y)| (13) NIL)
;∀X Y.X=Y⊃E0(X,Y)
;deps: (6)
;labels: XX
17. (ASSUME |∀X Y.Q2(X,Y)≡P1(X,Y)∨P2(X,Y)∨P3(X,Y)|)
;deps: (XX)
18. (DERIVE
|(∀X Y.P1(X,Y)⊃Q0(X,Y))∧(∀X Y.P2(X,Y)⊃Q0(X,Y))∧(∀X Y.P3(X,Y)⊃Q0(X,Y))⊃
(∀X Y.Q2(X,Y)⊃Q0(X,Y))| () (USE XX MODE: ALWAYS))
;(∀X Y.P1(X,Y)⊃Q0(X,Y))∧(∀X Y.P2(X,Y)⊃Q0(X,Y))∧(∀X Y.P3(X,Y)⊃Q0(X,Y))⊃
;(∀X Y.Q2(X,Y)⊃Q0(X,Y))
;deps: (XX)
19. (CI (XX) 18 NIL)
;(∀X Y.Q2(X,Y)≡P1(X,Y)∨P2(X,Y)∨P3(X,Y))⊃
;((∀X Y.P1(X,Y)⊃Q0(X,Y))∧(∀X Y.P2(X,Y)⊃Q0(X,Y))∧(∀X Y.P3(X,Y)⊃Q0(X,Y))⊃
; (∀X Y.Q2(X,Y)⊃Q0(X,Y)))
20. (UE
((P1.|λX Y.X=A∧Y=B|) (P2.|λX Y.X=B∧Y=A|) (P3.|λX Y.X=Y|) (Q0.|E0|)
(Q2.|E2|)) 19 NIL)
;(∀X Y.E2(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y)⊃
;((∀X Y.X=A∧Y=B⊃E0(X,Y))∧(∀X Y.X=B∧Y=A⊃E0(X,Y))∧(∀X Y.X=Y⊃E0(X,Y))⊃
; (∀X Y.E2(X,Y)⊃E0(X,Y)))
21. (DERIVE |∀X Y.E2(X,Y)⊃E0(X,Y)| (20 14 15 16) (OPEN E2))
;∀X Y.E2(X,Y)⊃E0(X,Y)
;deps: (6)
22. (DERIVE |∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))|
(10)
NIL)
;∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))
;deps: (6)
23. (UE ((E1.|E2|)) 22 NIL)
;AX(E2)∧(∀X Y.E2(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E2(X,Y))
;deps: (6)
24. (DERIVE |∀X Y.E0(X,Y)≡E2(X,Y)| (9 21 23) NIL)
;∀X Y.E0(X,Y)≡E2(X,Y)
;deps: (6)
25. (RW 24 (OPEN E2))
;∀X Y.E0(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y
;deps: (6)
26. (DERIVE |A≠B| (SIMPINFO) NIL)
;A≠B
27.
This proof uses circumscription to maximize the uniqueness of names, through
the circumscription of an equivalence relation e(x,y), which is to be
interpreted as asserting the equivalence of the objects denoted by x and y.
1. (axiom |index a =1 ∧ index b = 2 ∧ index c = 3 ∧ index d = 4|)
(label simpinfo)
Since EKL does not have attachments to determine the equivalence of names,
we establish a correspondence between the names in our domain and some
natural numbers. The label SIMPINFO on this statement and the next
indicates that these statements should be used by the EKL simplifier
whenever appropriate.
2. (der |¬(1=2) ∧ ¬(1=3) ∧ ¬(2=3) ∧ ¬(1=4) ∧ ¬(2=4) ∧ ¬ (3=4)|)
(label simpinfo)
EKL does know about the distinctness of natural numbers.
3. (DEFINE EQUIV
|∀E.EQUIV(E)≡
(∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))| NIL)
Here we state the conditions necessary for E to be an equivalence relation.
It must be reflexive, symmetric, and transitive.
4. (DEFINE ax |∀E.ax(E)≡E(A,B)∧EQUIV(E)| NIL)
This gives the property we want our equivalence relation e0 to have.
It must hold for two names a and b, and circumscription will be used
to make sure that it is the least equivalence relation holding for a and b.
The condition e(a,b) can be replaced by other similar conditions.
We define a property ax(e), because the proof must mention a specific
relation e2, which we will show has the same property.
5. (DEFINE ax1
|∀E.ax1(E)≡
ax(E)∧
(∀E1.ax(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))| NIL)
When we circumscribe a relation with property ax, we get a relation with
property ax1. It would be better to be able to write
(define ax1 |ax1 = circumscription(ax,e(x,y),x,y)|),
but we haven't yet specified what we want in general and checked whether EKL
can do it now or needs to be modified.
6. (ASSUME |ax1(E0)|)
deps: (6)
We now assume that e0 obeys the circumscription forumula. Many subsequent
statements will list 6 as a dependency because of this.
7. (DEFINE E2 |∀X Y.E2(X,Y)≡X=A∧Y=B∨x=b∧y=a∨X=Y| NIL)
We shall prove that ax1(e0) implies ∀xy.e0(x,y) ≡ e2(x,y), i.e. the
only equivalent pairs are (a,b), (b,a) and pairs in which both elements
are the same.
8. (DERIVE |EQUIV(E2)| () ((OPEN EQUIV) (OPEN E2)))
EQUIV(E2)
We infer that E2 is an equivalence relation. This takes EKL about 10 seconds
on the KL-10.
9. (DERIVE |ax(E2)| (8) ((OPEN ax) (OPEN E2)))
ax(E2)
10. (RW 6 (OPEN ax1))
ax(E0)∧(∀E1.ax(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
deps: (6)
Here we expand the circumscription formula.
11. (DERIVE |ax(E0)| (10) NIL)
ax(E0)
deps: (6)
This is merely the first conjunct of the previous statement.
12. (RW 11 (OPEN ax))
E0(A,B)∧EQUIV(E0)
deps: (6)
Expanding the definition of ax.
13. (RW 12 (OPEN EQUIV))
E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
deps: (6)
Expanding the definition of EQUIV
14. (DERIVE |∀X Y.E2(X,Y)⊃E0(X,Y)| (13) (OPEN E2))
14. (DERIVE |∀X Y.x=a∧y=b⊃E0(X,Y)| (13) (OPEN E2))
14. (DERIVE |∀X Y.x=a∧y=b⊃E0(X,Y)| (13)); 77 seconds
14. (DERIVE |∀X Y.x=b∧y=a⊃E0(X,Y)| (13)); 81 seconds
14. (DERIVE |∀X Y.x=y⊃E0(X,Y)| (13)); 7 seconds
∀X Y.E2(X,Y)⊃E0(X,Y)
deps: (6)
15. (DERIVE |∀E1.ax(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))|
(10) NIL)
∀E1.ax(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y))
deps: (6)
16. (UE ((E1.|E2|)) 15 NIL)
ax(E2)∧(∀X Y.E2(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E2(X,Y))
deps: (6)
The last three steps prove that E2 satisfies the circumscription formula.
17. (DERIVE |∀X Y.e0(X,Y)≡E2(X,Y)| (9 14 16) NIL)
∀X Y.e0(X,Y)≡E2(X,Y)
deps: (6)
Now we can find the set of equivalent pairs.
18. (RW 17 (OPEN E2))
∀X Y.E(X,Y)≡X=A∧Y=B∨X=Y
deps: (6)
19. (DERIVE |e0(A,B)| (18) NIL)
E(A,B)
deps: (6)
As before, A and B are equivalent.
20. (DERIVE |¬A=C| (SIMPINFO) NIL)
¬A=C
From the axioms at the beginning, we derive the uniqueness of names.
21. (DERIVE |¬B=C| (SIMPINFO) NIL)
¬B=C
22. (DERIVE |¬e0(A,C)| (18 20 21) NIL)
¬e0(A,C)
deps: (6)
This demonstrates that two names not explicitly stated to be equivalent
in our definition of ax(e0) are not equivalent.
.end
.skip 1
;labels: SIMPINFO
1. (AXIOM |INDEX(A)=1∧INDEX(B)=2∧INDEX(C)=3∧INDEX(D)=4|)
;labels: SIMPINFO
2. (DERIVE |¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬3=4| () NIL)
;¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬3=4
3. (DEFINE EQUIV
|∀E.EQUIV(E)≡
(∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))|
(NIL))
4. (DEFINE AX |∀E.AX(E)≡E(A,B)∧EQUIV(E)| (NIL))
5. (DEFINE AX1
|∀E.AX1(E)≡
AX(E)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))|
(NIL))
6. (ASSUME |AX1(E0)|)
;deps: (6)
7. (DEFINE E2 |∀X Y.E2(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y| (NIL))
8. (DERIVE |EQUIV(E2)| () ((OPEN EQUIV) (OPEN E2)))
;EQUIV(E2)
9. (DERIVE |AX(E2)| (8) ((OPEN AX) (OPEN E2)))
;AX(E2)
10. (RW 6 (OPEN AX1))
;AX(E0)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
;deps: (6)
11. (DERIVE |AX(E0)| (10) (NIL))
;AX(E0)
;deps: (6)
12. (RW 11 (OPEN AX))
;E0(A,B)∧EQUIV(E0)
;deps: (6)
13. (RW 12 (OPEN EQUIV))
;E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
;deps: (6)
14. (DERIVE |∀X Y.X=A∧Y=B⊃E0(X,Y)| (13) (OPEN E2))
;∀X Y.X=A∧Y=B⊃E0(X,Y)
;deps: (6)
15. (TRW |∀X Y.X=A∧Y=B⊃E0(X,Y)| ((USE 13) (OPEN E2)))
;(∀X Y.X=A∧Y=B⊃E0(X,Y))≡(∀X Y.X=A∧Y=B⊃E0(X,Y))
;deps: (6)
16. (DERIVE |∀X Y.X=A∧Y=B⊃E0(X,Y)| (13) NIL)
;∀X Y.X=A∧Y=B⊃E0(X,Y)
;deps: (6)
17. (DERIVE |∀X Y.X=Y⊃E0(X,Y)| (13) NIL)
;∀X Y.X=Y⊃E0(X,Y)
;deps: (6)
18. (DERIVE |∀X Y.X=B∧Y=A⊃E0(X,Y)| (13) NIL)
;∀X Y.X=B∧Y=A⊃E0(X,Y)
;deps: (6)
19.
;labels: SIMPINFO
1. (AXIOM |INDEX(A)=1∧INDEX(B)=2∧INDEX(C)=3∧INDEX(D)=4|)
;labels: SIMPINFO
2. (DERIVE |¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4| () NIL)
;¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4
3. (DERIVE |A≠B| (SIMPINFO) NIL)
;A≠B
4. (DEFINE EQUIV
|∀E.EQUIV(E)≡
(∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))|
NIL)
5. (DEFINE AX |∀E.AX(E)≡E(A,B)∧EQUIV(E)| NIL)
6. (DEFINE AX1
|∀E.AX1(E)≡
AX(E)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))|
NIL)
;labels: CIRCUM
7. (ASSUME |AX1(E0)|)
;deps: (CIRCUM)
8. (DEFINE E2 |∀X Y.E2(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y| NIL)
9. (DERIVE |EQUIV(E2)| () ((OPEN EQUIV) (OPEN E2)))
;EQUIV(E2)
;labels: AX_E2
10. (DERIVE |AX(E2)| (9) ((OPEN AX) (OPEN E2)))
;AX(E2)
11. (RW CIRCUM (OPEN AX1))
;AX(E0)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
;deps: (CIRCUM)
12. (TRW |AX(E0)| (USE 11))
;AX(E0)
;deps: (CIRCUM)
;labels: FACT1
13. (RW 12 (OPEN AX EQUIV))
;E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
;deps: (CIRCUM)
;labels: REWRITE_BY_CASES
14. (DERIVE |∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)| () NIL)
;∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)
15. (TRW |∀X Y.E2(X,Y)⊃E0(X,Y)|
((OPEN E2) (USE REWRITE_BY_CASES MODE: ALWAYS) (USE FACT1)))
;(∀X Y.E2(X,Y)⊃E0(X,Y))≡(∀X Y.(X=A∧Y=B⊃E0(X,Y))∧(X=B∧Y=A⊃E0(X,Y)))
;deps: (CIRCUM)
16.